\chapter{Orders of magnitude}\label{ch:order_of_magnitude}

The hyperreals ${}^* \R$ are already defined in Mathlib, using a Lean-canonically chosen ultrafilter on $\N$.  One could consider generalizing the hyperreal construction to other filters or ultrafilters, but given the extensive library support for the Mathlib hyperreals, and the fact that it already enjoys enough of a transfer principle for most applications, we will base our theory here on the Mathlib hyperreals.

\begin{definition}[Positive hyperreals]\label{pos-hyperreal}\lean{PositiveHyperreal, PositiveHyperreal.lesssim, PositiveHyperreal.ll}\leanok  The positive hyperreals ${}^* \R^+$ are the set of hyperreals $X \in {}^* \R$ such that $X > 0$.  (Note that $X$ could be infinitesimal or infinite).

If $X,Y$ are positive hyperreals, we write $X \lesssim Y$ if $X \leq CY$ for some real $C>0$.  We write $X \asymp Y$ if $X \lesssim Y \lesssim X$.  We write $X \ll Y$ if $X \leq \eps Y$ for all real $\eps>0$.
\end{definition}

\begin{lemma}[Lesssim order]\label{lesssim-order}\uses{pos-hyperreal}\lean{PositiveHyperreal.asym_preorder}\leanok  $\lesssim$ is a pre-order on ${}^* \R^+$, with $\asymp$ the associated equivalence relation, and $\ll$ the associated strict order.  Any two positive hyperreals are comparable under $\lesssim$.
\end{lemma}

\begin{proof}\leanok Easy.
\end{proof}

\begin{definition}[Orders of magnitude]\label{ord-def}\uses{lesssim-order}\lean{OrderOfMagnitude,PositiveHyperreal.order,PositiveHyperreal.order_surjective}\leanok The space $\O$ of orders of magnitude is defined to be the quotient space ${}^* \R^+ / \asymp$ of the positive hyperreals by the relation of asymptotic equivalence.  For a positive hyperreal $X$, we let $\Theta(X)$ denote the order of magnitude of $X$; this is a surjection from ${}^* \R^+$ to $\O$.
\end{definition}


\begin{lemma}[Theta kernel]\label{theta-kernel}\uses{ord-def}\lean{PositiveHyperreal.order_eq_iff, PositiveHyperreal.order_le_iff, PositiveHyperreal.order_lt_iff}\leanok For positive hyperreals $X,Y$, we have $\Theta(X) = \Theta(Y)$ if and only if $X \asymp Y$.  Similarly, we have $\Theta(X) < \Theta(Y)$ if and only if $X \ll Y$, and $\Theta(X) \leq \Theta(Y)$ if and only if $X \lesssim Y$.
\end{lemma}

\begin{proof}\leanok Easy.
\end{proof}

\begin{definition}[Ordering on magnitudes]\label{ord-mag-def}\uses{theta-kernel}\lean{OrderOfMagnitude.linearOrder}\leanok  We linearly order $\O$ by the requirement that $\Theta(X) \leq \Theta(Y)$ if and only if $X \lesssim Y$, and  $\Theta(X) < \Theta(Y)$ if and only if $X \ll Y$.
\end{definition}

\begin{definition}[One]\label{one-def}\uses{ord-def}\label{OrderOfMagnitude.one}\leanok We define $1 := \Theta(1)$.
\end{definition}

\begin{lemma}[Constants trivial]\label{const-triv}\uses{one-def}\lean{Real.order_of_pos}\leanok We have $\Theta(C) = 1$ for all real $C>0$.
\end{lemma}

\begin{proof}\leanok Easy.
\end{proof}

\begin{definition}[Arithmetic on magnitudes]\label{mag-arith}\uses{theta-kernel}\lean{OrderOfMagnitude.add, OrderOfMagnitude.mul, OrderOfMagnitude.pow}\leanok  We define addition on $\O$ by the requirement that $\Theta(X) + \Theta(Y) = \Theta(X+Y)$ for positive hyperreals $X,Y$.  Similarly we define multiplication, inverse, and division.  We define real exponentiation by requiring that $\Theta(X^\alpha) = \Theta(X)^\alpha$ for positive hyperreals $X$ and real $\alpha$.
\end{definition}

\begin{lemma}[Addition is tropical]\label{tropical-add}\uses{mag-arith}\lean{OrderOfMagnitude.add_eq_max}\leanok For all orders of magnitude $\Theta(X), \Theta(Y)$, we have $\Theta(X) + \Theta(Y) = \max(\Theta(X), \Theta(Y))$.
\end{lemma}

\begin{proof}\leanok Easy.
\end{proof}

\begin{corollary}[Additive commutative monoid]\label{add-comm-mon}\uses{tropical-add}\lean{OrderOfMagnitude.addCommSemigroup, OrderOfMagnitude.add_self}\leanok $\O$ is an ordered additive idempotent commutative monoid.
\end{corollary}

\begin{proof}\leanok Easy.
\end{proof}

\begin{lemma}[Commutative semiring]\label{comm-semiring}\uses{mag-arith}\lean{OrderOfMagnitude.distrib, OrderOfMagnitude.comm_group, OrderOfMagnitude.orderedMonoid}\leanok $\O$ is a multiplicative ordered commutative group that distributes over addition.  (It is not a semiring in the Mathlib sense because it does not have a zero element.)
\end{lemma}

\begin{proof}\uses{tropical-add}\leanok Easy.
\end{proof}

\begin{lemma}[Power laws]\label{power-law}\uses{mag-arith}\lean{power_i,power_i', power_ii, power_iv, power_v, power_vi, power_vii, power_vii', power_viii, power_ix, power_ix'}  Let $\Theta(X), \Theta(Y)$ be orders of magnitude, and $\alpha,\beta$ be real numbers.
    \begin{itemize}
    \item[(i)] We have $\Theta(XY)^\alpha = \Theta(X^\alpha Y^\alpha)$ and $\Theta(X/Y)^\alpha = \Theta(X^\alpha / Y^\alpha)$.
    \item[(ii)] We have $\Theta(X^{\alpha \beta}) = \Theta(X^\alpha)^\beta$.  
    \item[(iii)] We have $\Theta(X)^0 = 1$, $\Theta(X)^1 = \Theta(X)$, and $\Theta(X)^{-1} = 1 / \Theta(X)$.
    \item[(iv)] We have $\Theta(1)^\alpha = 1$.
    \item[(v)] We have $\Theta(X+Y)^\alpha = \Theta(X)^\alpha + \Theta(Y)^\alpha$ for $\alpha \geq 0$.
    \item[(vi)]  If $\alpha \geq 0$ and $\Theta(X) \leq \Theta(Y)$, then $\Theta(X)^\alpha \leq \Theta(Y)^\alpha$.
    \item[(vii)] If $\alpha > 0$, then $\Theta(X) \leq \Theta(Y)$, if and only if $\Theta(X)^\alpha \leq \Theta(Y)^\alpha$, and $\Theta(X) < \Theta(Y)$ if and only if $\Theta(X)^\alpha < \Theta(Y)^\alpha$.
    \item[(viii)] If $\alpha \leq 0$ and $\Theta(X) \leq \Theta(Y)$, then $\Theta(X)^\alpha \geq \Theta(Y)^\alpha$.
    \item[(ix)] If $\alpha < 0$, then $\Theta(X) \leq \Theta(Y)$, if and only if $\Theta(X)^\alpha \geq \Theta(Y)^\alpha$, and $\Theta(X) < \Theta(Y)$ if and only if $\Theta(X)^\alpha > \Theta(Y)^\alpha$.   
    \end{itemize}
\end{lemma}

\begin{proof} Straightforward.
\end{proof}

\begin{definition}[Log-order of magnitude] \label{log-order-def}\uses{mag-arith}\lean{LogOrderOfMagnitude, OrderOfMagnitude.log, LogOrderOfMagnitude.exp, OrderOfMagnitude.log_ordered, LogOrderOfMagnitude.exp_ordered}\leanok  We define $\log \O$ to be the collection of formal logarithms of magnitude $\log(\Theta(X))$ of orders of magnitude $\Theta(X)$.  $1$, multiplication, and exponentiation of orders of magnitude become $0$, addition, and scalar multiplication; and order is preserved. By definition, $\log \colon \O \to \log \O$ is a order isomorphism.
\end{definition}


\begin{lemma}[Log of addition]\label{log-add}\uses{log-order-def}\lean{OrderOfMagnitude.log_mul, OrderOfMagnitude.log_mul'}\leanok  For orders of magnitude $\Theta(X), \Theta(Y)$, we have $\log(\Theta(X) + \Theta(Y)) = \max(\log(\Theta(X)), \log(\Theta(Y)))$.
\end{lemma}

\begin{proof}\uses{tropical-add} Immediate from Lemma \ref{tropical-add}.
\end{proof}

\begin{lemma}[Logarithm of multiplication and exponentiation]\label{log-mult}  For orders of magnitude $\Theta(X), \Theta(Y)$, we have $\log(1) = 0$ (and more generally $\log(C) = 0$ for any real $C>0$), $\log(\Theta(X) \Theta(Y)) = \log(\Theta(X)) + \log(\Theta(Y))$, and $\log(\Theta(X) / \Theta(Y)) = \log(\Theta(X)) - \log(\Theta(Y))$.  For any real $\alpha$, we have $\log(\Theta(X)^\alpha) = \alpha \log(\Theta(X))$.
\end{lemma}

\begin{proof}\uses{mag-arith, power-law}. Straightforward from Lemma \ref{mag-arith} and Lemma \ref{power-law}.
\end{proof}


\begin{lemma}[Ordered vector space]\label{ord-vec}\uses{log-order-def}\lean{LogOrderOfMagnitude.vec, LogOrderOfMagnitude.posSMulStrictMono} $\log \O$ is a linearly ordered real vector space.
\end{lemma}

\begin{proof}\uses{log-mult} Straightforward from Lemma \ref{log-mult}.
\end{proof}

\begin{lemma}[Countable saturation]\label{saturation}\lean{saturation}\leanok Let $I_1 \supset I_2 \supset \dots$ be a sequence of internal sets in the hyperreals.  If each of the $I_n$ is non-empty, then $\bigcap_{n=1}^\infty I_n$ is non-empty.
\end{lemma}

\begin{proof}  Write each $I_n$ as an ultraproduct of $I_{n,m}$.  Then, we can find a nested sequence $E_1 \supset E_2 \supset \dots$ of large sets in the ultrafilter such that $\bigcap_{n \leq n_0} I_{n,m}$ is non-empty for all $m \in E_{n_0}$ and all $n_0$, and also $n_0 \not \in E_{n_0}$.  If we then pick $x_m$ to lie in $\bigcap_{n \leq n_0} E_{n,m}$ where $n_0$ is the largest number for which $m \in E_{n_0}$, the ultralimit of the $x_m$ will have the required properties.
\end{proof}

\begin{lemma}[Completeness]\label{completeness} Let $I_1 \supset I_2 \supset \dots$ be a decreasing sequence of non-empty open intervals (possibly unbounded) in $\O$.  Then $\bigcap_{n=1}^\infty I_n$ is non-empty.
\end{lemma}

\begin{proof}\uses{saturation} Pull back each of the $I_n$ to the hyperreals as a countable intersection of internal sets, and apply Lemma \ref{saturation}.
\end{proof}

\begin{lemma}[Completeness, II]\label{completeness-2} Let $I_1 \supset I_2 \supset \dots$ be a decreasing sequence of non-empty intervals (possibly unbounded or closed) in $\O$.  Then $\bigcap_{n=1}^\infty I_n$ is non-empty.
\end{lemma}

\begin{proof} \uses{completeness}  If one of the $I_n$ is a singleton, the claim is straightforward.  Otherwise, replace each $I_n$ by its interior and use Lemma \ref{completeness}.
\end{proof}


